lemma extensional_eq : (fun (x : int) -> x = x) = (fun y -> y = y)
